T:Type, P:(T), L1, L2:(T List).
no_repeats(T;L1)
 no_repeats(T;L2)
 ((filter(P;L1) = L2)
  ((x:T. (x  L2)  ((x  L1) & ((P(x)))))
  & (x, y:T. x before y  L2  x before y  L1))) 

latex

Definitions

Type, , P  Q, x before y  l, x:A. B(x), P  Q, P & Q, x:A  B(x), b, (x  l), s = t, no_repeats(T;l), x:AB(x), t  T, type List, {T}, False, Dec(P), P  Q, P  Q, , [], f(a), left + right, Unit, , , {x:A| B(x)} , A  B, A, a < b, ||as||, Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), n+m, l[i], hd(l), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j, b, i <z j, if a<b then c else d, n - m, tl(l), [car / cdr], #$n, Void, L1  L2, {i..j}, i  j < k, increasing(f;k), reduce(f;k;as), filter(P;l), i  j , A c B, x. t(x), T, s ~ t, SQType(T), True

Lemmas

not assert elim, bool sq, true wf, squash wf, l before member2, l before member, all functionality wrt iff, cons before, implies functionality wrt iff, or functionality wrt iff, iff functionality wrt iff, and functionality wrt iff, length wf1, non neg length, hd wf, ge wf, tl wf, no repeats cons, filter wf, false wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, cons member, l member wf, no repeats wf, l before wf, assert wf, iff wf, decidable assert, nil member, bool wf